 
-- November 13

--
--  SSL 3.0 model
--
--  Vitaly Shmatikov
--

--
-- Parameters
--

const
  UseClientNonces:		true;
  UseServerNonces:		true;
  ServerFullCertificateCheck:	false;
  ServerSignCertificateCheck:	true;
  ServerSignatureCheck:		true;
  ClientCertificateCheck:	true;
  ClientSignatureCheck:		true;
  ServerVersionCheckInKey:	true;
  ServerKeyCheckInVerify:	true;
  ServerLogCheckInVerify:	false;
  ClientLogCheckInFinished:	true;
  ServerLogCheckInFinished:	true;

  ClientAuthenticationInSSL2:	true;

  -- Intruder behavior
  IntruderMayInitiate:		false;

  MaxRepeatRuns:	1;
  MaxSessionId:		1;

  NumClients:		1;
  NumServers:		1;
  NumIntruders: 	1;
  NetworkSize:		1;

  MaxRandom:		20;
  MaxNonce:		10;

  -- What intruder can remember
  MaxMessages:		50;
  MaxPublicKeys:	10;
  MaxVerifKeys:		10;
  MaxSecretKeys:	10;
  MaxHandshakeLogs:	10;

  MaxVersion:		3;

--
-- Players
--

type
  ClientId:	scalarset (NumClients);
  ServerId:	scalarset (NumServers);
  IntruderId:	scalarset (NumIntruders);
  AgentId:	union {ClientId, ServerId, IntruderId};

  Random:		0..MaxRandom;
  Nonce:		0..MaxNonce;
  SessionId:		0..MaxSessionId;
  ValidSessionId:	1..MaxSessionId;
  Version:		1..MaxVersion;

-- Key modeling

KeyType: enum {
  K_ENCRYPT,
  K_VERIFY
};

Key: record
  kType:        KeyType;
  random:	Random;
end;

Certificate: record
  key:          Key;
  owner: 	AgentId;
  signKey:	Key;
end;

CertifiedKey: record
  key: 	Key;
  cert:	Certificate;
end;

PlainText: record
  text:	0..1;
end;

--
-- Message modeling
--

MessageType: enum {
  M_CLIENT_HELLO,
  M_CLIENT_HELLO_RESUME,
  M_SERVER_HELLO,
  M_SERVER_KEY_EXCHANGE,
  M_CLIENT_KEY_EXCHANGE,
  M_SERVER_ACK_KEY,
  M_CLIENT_VERIFY,
  M_SERVER_FINISHED,
  M_CLIENT_FINISHED,

  -- SSL2 messages
  M_2_SERVER_CERTIFICATE_REQUEST,
  M_2_CLIENT_CERTIFICATE,
  M_2_CLIENT_FINISHED,
  M_2_SERVER_FINISHED,

  -- Phantom message types: needed for state encoding
  M_SERVER_SEND_KEY,
  M_SERVER_SEND_FINISHED,
  M_SLEEP,
  M_DONE
};

HandshakeRecord: record
    session:		ValidSessionId;
    clientVersion:	Version;
    clientSuite:	PlainText;
    clientNonce:	Nonce;
--  clientVerifKey:	CertifiedKey;
    secretKey:		Key;
--  clientSender:	ClientId;

    serverVersion:	Version;
    serverSuite:	PlainText;
    serverNonce:	Nonce;
--  serverPublicKey:	CertifiedKey;
--  serverVerifKey:	CertifiedKey;
--  serverSender:	ServerId;
end;

Message: record
  session:	SessionId;
  source:	AgentId;
  dest:		AgentId;
  mType:	MessageType;

  version:	Version;
  suite:	PlainText;
  nonce:	Nonce;
  publicKey:	CertifiedKey;
  verifKey:	CertifiedKey;
  secretKey:    Key;
  handshakeLog:	HandshakeRecord;
  encKey:       Key;
  signKey:	Key;
  encSession:	ValidSessionId;

  fromIntruder: boolean;
end;

-- M_CLIENT_HELLO: version, suite, nonce
-- M_CLIENT_HELLO_RESUME: version, suite, nonce
-- M_SERVER_HELLO: version, suite, nonce
-- M_SERVER_KEY_EXCHANGE: publicKey, verifKey, signKey
-- M_CLIENT_KEY_EXCHANGE: version, secretKey, encKey
-- M_SERVER_ACK_KEY:
-- M_CLIENT_VERIFY: verifKey, handshakeLog (hashed), signKey
-- M_SERVER_FINISHED: handshakeLog (hashed), encKey
-- M_CLIENT_FINISHED: handshakeLog (hashed), encKey
--
-- M_2_SERVER_CERTIFICATE_REQUEST: nonce, encKey
-- M_2_CLIENT_CERTIFICATE: verifKey, nonce, signKey, encKey
-- M_2_CLIENT_FINISHED: nonce, encKey
-- M_2_SERVER_FINISHED: nonce, encSession, encKey

--
-- Player modeling
--

-- If state = M_X,
-- then the party is ready to receive message of type M_X

-- Client

Client: record
  authKey:		Key;		-- Sig. authority's verif. key
  version:		Version;        -- Client's version
  suite:		PlainText;      -- Client's crypto suite
  verifKey:             CertifiedKey;   -- Verification key

  state:		MessageType;
  secretKey:    	Key;		-- Shared secret
  nonce:		Nonce;
  session:		SessionId;
  resumeSession:	boolean;

  server:		AgentId;
  serverVersion: 	Version;        -- Server's version
  serverSuite:		PlainText;      -- Server's crypto suite
  serverNonce:		Nonce;		-- Server's nonce
  serverPublicKey:	CertifiedKey;	-- Server's public key
  serverVerifKey:	CertifiedKey;	-- Server's verification key
end;

-- Server

SessionState: record
  state:		MessageType;
  client:		AgentId;	-- Client of this session
  nonce:		Nonce;		-- Nonce for this session
  secretKey:    	Key;		-- Shared secret
  clientVerifKey:	CertifiedKey;
  clientVersion:	Version;
  clientSuite:		PlainText;	-- Client's crypto suite
  clientNonce:		Nonce;
  challenge:		Nonce;		-- Client challenge (SSL2)
  resumeSession:	boolean;        -- Resumed session?
end;

Server: record
  clients: 	array[SessionId] of SessionState;
  authKey:	Key;		-- Sig. authority's verif. key
  version:	Version;        -- Server's version
  suite:	PlainText;      -- Server's suite
  publicKey:   	CertifiedKey;
  verifKey:   	CertifiedKey;
end;

-- Intruder

Intruder: record
  goodVersion:	Version;
  evilVersion:	Version;
  goodSuite:	PlainText;      -- Good crypto suite
  evilSuite:	PlainText;      -- Evil crypto suite

  publicKey:    CertifiedKey;
  verifKey:     CertifiedKey;
  messages:	multiset[MaxMessages] of Message;
  nonces:	multiset[MaxNonce] of Nonce;
  publicKeys:	multiset[MaxPublicKeys] of CertifiedKey;
  verifKeys:	multiset[MaxVerifKeys] of CertifiedKey;
  secretKeys:	multiset[MaxSecretKeys] of Key;
  logs:		multiset[MaxHandshakeLogs] of HandshakeRecord;
  clientCerts:	multiset[MaxMessages] of Message;
end;

var
  cliNet:	multiset[NetworkSize] of Message;
  serNet:  	multiset[NetworkSize] of Message;
  cli:  	array[ClientId] of Client;
  ser:  	array[ServerId] of Server;
  int:  	array[IntruderId] of Intruder;

  runCount:		array[ClientId] of 0..MaxRepeatRuns;
  SessionBound: 	ValidSessionId;
  RunModel:		boolean;
  NoMoreSessions:	boolean;

  nextRandom:	Random;
  nextNonce:	Nonce;
  nextSession:	SessionId;


-- Generate a fresh random number

function freshRandom(): Random;
var tmp: Random;
begin
   if nextRandom = MaxRandom then
      error "Ran out of random numbers!"
   end;
   tmp := nextRandom;
   nextRandom := nextRandom + 1;
   return tmp;
end;

-- Generate a fresh nonce

function freshNonce(): Nonce;
var tmp: Nonce;
begin
   if nextNonce = MaxNonce then
      error "Ran out of nonces!"
   end;
   tmp := nextNonce;
   nextNonce := nextNonce + 1;
   return tmp;
end;

-- Generate a fresh session id

function freshSessionId(): SessionId;
begin
   if !NoMoreSessions then
      nextSession := nextSession + 1;
      if nextSession = SessionBound then
         NoMoreSessions := true;
      end;
      return nextSession;
   else
      return 0;
   end;
end;

--
-- Comparison functions
--

function keyEqual(key1: Key; key2: Key): boolean;
begin
   return (key1.kType  = key2.kType) &
          (key1.random = key2.random);
end;

function certEqual(cert1: Certificate; cert2: Certificate): boolean;
begin
   return keyEqual(cert1.key, cert2.key) &
          (ClientCertificateCheck & ismember(cert1.owner, ClientId) ->
           cert1.owner = cert2.owner) &
          ((ServerFullCertificateCheck |
            ServerSignCertificateCheck) & ismember(cert1.owner, ServerId) ->
           cert1.owner = cert2.owner) &
          keyEqual(cert1.signKey, cert2.signKey);
end;

function certKeyEqual(ck1: CertifiedKey; ck2: CertifiedKey): boolean;
begin
   return keyEqual(ck1.key, ck2.key) &
          certEqual(ck1.cert, ck2.cert);
end;

function plainEqual(p1: PlainText; p2: PlainText): boolean;
begin
   return (p1.text = p2.text);
end;

function logEqual(l1: HandshakeRecord; l2: HandshakeRecord): boolean;
begin
   return (l1.session       = l2.session) &
          (l1.clientVersion = l2.clientVersion) &
          plainEqual(l1.clientSuite, l2.clientSuite) &
          (l1.clientNonce   = l2.clientNonce) &
          (l1.serverVersion = l2.serverVersion) &
          (l1.serverNonce   = l2.serverNonce) &
          keyEqual(l1.secretKey, l2.secretKey);
          -- (l1.clientSender  = l2.clientSender) &
          -- (l1.serverSender  = l2.serverSender);
end;

function msgEqual(msg1: Message; msg2: Message): boolean;
var
   res: boolean;
begin
   res := false;
   if (msg1.source       = msg2.source) &
      (msg1.dest         = msg2.dest) &
      (msg1.mType        = msg2.mType) &
      (msg1.fromIntruder = msg2.fromIntruder) &
      (msg1.session      = msg2.session) then
      switch msg1.mType
         case M_CLIENT_HELLO:
            res := (msg1.version = msg2.version) &
                   plainEqual(msg1.suite, msg2.suite) &
                   (msg1.nonce   = msg2.nonce);
         case M_CLIENT_HELLO_RESUME:
            res := (msg1.version = msg2.version) &
                   plainEqual(msg1.suite, msg2.suite) &
                   (msg1.nonce   = msg2.nonce);
         case M_SERVER_HELLO:
            res := (msg1.version = msg2.version) &
                   plainEqual(msg1.suite, msg2.suite) &
                   (msg1.nonce   = msg2.nonce);
         case M_SERVER_KEY_EXCHANGE:
            res := certKeyEqual(msg1.publicKey, msg2.publicKey) &
                   certKeyEqual(msg1.verifKey,  msg2.verifKey) &
                       keyEqual(msg1.signKey,   msg2.signKey);
         case M_CLIENT_KEY_EXCHANGE:
            res := (msg1.version = msg2.version) &
                   keyEqual(msg1.secretKey, msg2.secretKey) &
                   keyEqual(msg1.encKey, msg2.encKey);
         case M_SERVER_ACK_KEY:
            res := true;
         case M_CLIENT_VERIFY:
            res := certKeyEqual(msg1.verifKey, msg2.verifKey) &
                   logEqual(msg1.handshakeLog, msg2.handshakeLog) &
                   keyEqual(msg1.signKey,      msg2.signKey);
         case M_SERVER_FINISHED:
            res := logEqual(msg1.handshakeLog, msg2.handshakeLog) &
                   keyEqual(msg1.encKey, msg2.encKey);
         case M_CLIENT_FINISHED:
            res := logEqual(msg1.handshakeLog, msg2.handshakeLog) &
                   keyEqual(msg1.encKey, msg2.encKey);
         case M_2_SERVER_CERTIFICATE_REQUEST:
            res := (msg1.nonce = msg2.nonce) &
                   keyEqual(msg1.encKey, msg2.encKey);
         case M_2_CLIENT_CERTIFICATE:
            res := certKeyEqual(msg1.verifKey, msg2.verifKey) &
                   (msg1.nonce = msg2.nonce) &
                   keyEqual(msg1.signKey, msg2.signKey) &
                   keyEqual(msg1.encKey,  msg2.encKey);
         case M_2_CLIENT_FINISHED:
            res := (msg1.nonce = msg2.nonce) &
                   keyEqual(msg1.encKey, msg2.encKey);
         case M_2_SERVER_FINISHED:
            res := (msg1.nonce      = msg2.nonce) &
                   (msg1.encSession = msg2.encSession) &
                   keyEqual(msg1.encKey, msg2.encKey);
      end;
   end;
   return res;
end;


-----------
-- Rules --
-----------


--
-- Clients
--


-- Client sends ClientHello to a server (new session)

ruleset i: ClientId do
  ruleset j: ServerId do
    rule 10 "Client sends ClientHello to server (new session)"

      cli[i].state = M_SLEEP &
      cli[i].resumeSession  = false &
      multisetcount(l:cliNet, true) < NetworkSize &
      multisetcount(l:serNet, true) < NetworkSize &
      RunModel

    ==>

    var
      outM: Message;  -- outgoing message

    begin
      undefine outM;
      outM.source       := i;
      outM.dest         := j;
      outM.session      := 0;
      outM.fromIntruder := false;
      outM.mType        := M_CLIENT_HELLO;

      outM.version      := cli[i].version;
      outM.suite        := cli[i].suite;
      cli[i].nonce := freshNonce();
      outM.nonce        := cli[i].nonce;

      multisetadd (outM, cliNet);

      cli[i].server := j;
      cli[i].state  := M_SERVER_HELLO;
    end;

  end;
end;

-- Client sends ClientHello to a server (resume an existing session)

ruleset i: ClientId do
  rule 10 "Client sends ClientHello to server (resume session)"

    cli[i].state = M_SLEEP &
    cli[i].resumeSession  = true &
    multisetcount(l:cliNet, true) < NetworkSize &
    multisetcount(l:serNet, true) < NetworkSize &
    RunModel

  ==>

  var
    outM: Message;  -- outgoing message

  begin
    undefine outM;
    outM.source       := i;
    outM.dest         := cli[i].server;
    outM.session      := cli[i].session;
    outM.fromIntruder := false;
    outM.mType        := M_CLIENT_HELLO_RESUME;

    outM.version      := cli[i].version;
    outM.suite        := cli[i].suite;
    cli[i].nonce := freshNonce();
    outM.nonce        := cli[i].nonce;

    multisetadd (outM, cliNet);

    cli[i].state := M_SERVER_HELLO;
  end;

end;

-- Client receives ServerHello.
-- SSL3:
--    full session:      wait for ServerKeyExchange
--    resumed session:   wait for ServerFinished
-- SSL2:
--    send ClientFinished 

ruleset i: ClientId do
  choose l: cliNet do
    rule 10 "Client receives ServerHello, then waits for ServerKeyExchange (SSL3, full session), ServerFinished (SSL3, resumed session), or sends ClientFinished to server (SSL2)"

       cli[i].state = M_SERVER_HELLO &
       cliNet[l].dest = i &
       multisetcount(l:serNet, true) < NetworkSize &
       RunModel

    ==>

    var
      inM:  Message;  -- incoming message
      outM: Message;  -- outgoing message
    
    begin
      inM := cliNet[l];
      multisetremove(l, cliNet);

      if inM.mType = M_SERVER_HELLO then

         if (inM.session > 0) then

            if (cli[i].resumeSession = false) then

               -- New session

               cli[i].session       := inM.session;
               cli[i].serverVersion := inM.version;
               cli[i].serverSuite   := inM.suite;
               cli[i].serverNonce   := inM.nonce;

               cli[i].state := M_SERVER_KEY_EXCHANGE;

            else

               -- Resumed session

               if (cli[i].session = inM.session) then

                  -- Are these fields actually used?
                  cli[i].serverVersion := inM.version;
                  cli[i].serverSuite   := inM.suite;
                  --
                  cli[i].serverNonce   := inM.nonce;

                  if cli[i].serverVersion = MaxVersion then

		     -- SSL 3.0

                     cli[i].state := M_SERVER_FINISHED;

                  else

		     -- SSL 2.0

                     undefine outM;
                     outM.source       := i;
                     outM.dest         := cli[i].server;
                     outM.session      := cli[i].session;
                     outM.fromIntruder := false;
                     outM.mType        := M_2_CLIENT_FINISHED;

		     outM.nonce        := cli[i].serverNonce;
		     outM.encKey       := cli[i].secretKey;

                     multisetadd (outM, cliNet);

                     if ClientAuthenticationInSSL2 then
                        cli[i].state := M_2_SERVER_CERTIFICATE_REQUEST;
                     else
                        cli[i].state := M_2_SERVER_FINISHED;
                     end;

                  end
               
               else
                  -- Inconsistent session number
                  RunModel := false;
               end;
            end;
         
         else
            -- Server could not create a new session
            RunModel := false;
         end;
      else
         -- M_SERVER_HELLO expected
         RunModel := false;
      end;
    end;

  end;
end;

-- Client receives ServerKeyExchange and sends ClientKeyExchange to server

ruleset i: ClientId do
  choose l: cliNet do
    rule 10 "Client receives public key (ServerKeyExchange) and sends an encrypted secret (ClientKeyExchange) to server"

       cli[i].state = M_SERVER_KEY_EXCHANGE &
       cliNet[l].dest = i &
       multisetcount(l:serNet, true) < NetworkSize &
       RunModel

    ==>

    var
      inM:  Message;  -- incoming message
      outM: Message;  -- outgoing message
    
    begin
      inM := cliNet[l];
      multisetremove(l, cliNet);

      if inM.mType = M_SERVER_KEY_EXCHANGE then

         if ((ServerFullCertificateCheck ->

             -- Check public key certificate
             keyEqual(inM.publicKey.key, inM.publicKey.cert.key) &
             (cli[i].server  = inM.publicKey.cert.owner) &
             keyEqual(cli[i].authKey, inM.publicKey.cert.signKey)) &

             (ServerSignCertificateCheck ->

             -- Check verification key certificate
             keyEqual(inM.verifKey.key, inM.verifKey.cert.key) &
             (cli[i].server = inM.verifKey.cert.owner) &
             keyEqual(cli[i].authKey, inM.verifKey.cert.signKey) &

                (ServerSignatureCheck ->

                -- Check server's signature
                keyEqual(inM.verifKey.key, inM.signKey)))) then

            cli[i].serverPublicKey := inM.publicKey;
            cli[i].serverVerifKey  := inM.verifKey;
         
            undefine outM;
            outM.source       := i;
            outM.dest         := cli[i].server;
            outM.session      := cli[i].session;
            outM.fromIntruder := false;
            outM.mType        := M_CLIENT_KEY_EXCHANGE;
   
            outM.version      := cli[i].version;
            -- Generate a fresh secret key
            undefine cli[i].secretKey;
            cli[i].secretKey.kType  := K_ENCRYPT;
            cli[i].secretKey.random := freshRandom();
            outM.secretKey    := cli[i].secretKey;
            -- Encrypt with server's public key
            outM.encKey       := cli[i].serverPublicKey.key;
            
            multisetadd (outM, cliNet);
            
            cli[i].state := M_SERVER_ACK_KEY;
        
         else
            -- Invalid certificate or signature for server's key
            RunModel := false;
         end;

      else
         -- M_SERVER_KEY_EXCHANGE expected
         RunModel := false;
      end;
    end;

  end;
end;

-- Client receives server's ack and sends CertificateVerify to server

ruleset i: ClientId do
  choose l: cliNet do
    rule 10 "Client receives server's key exchange ack and sends a verification key certificate and signed hash of previous messages (CertificateVerify) to server"

       cli[i].state = M_SERVER_ACK_KEY &
       cliNet[l].dest = i &
       multisetcount(l:serNet, true) < NetworkSize &
       RunModel &
       cli[i].serverVersion = MaxVersion

    ==>

    var
      inM:  Message;  -- incoming message
      outM: Message;  -- outgoing message
    
    begin
      inM := cliNet[l];
      multisetremove(l, cliNet);

      if inM.mType = M_SERVER_ACK_KEY then

         undefine outM;
         outM.source       := i;
         outM.dest         := cli[i].server;
         outM.session      := cli[i].session;
         outM.fromIntruder := false;
         outM.mType        := M_CLIENT_VERIFY;

         outM.verifKey     := cli[i].verifKey;
         -- Log of previous handshake messages
         outM.handshakeLog.session       := cli[i].session;
         outM.handshakeLog.clientVersion := cli[i].version;
         outM.handshakeLog.clientSuite   := cli[i].suite;
         outM.handshakeLog.clientNonce   := cli[i].nonce;
         outM.handshakeLog.serverVersion := cli[i].serverVersion;
         outM.handshakeLog.serverSuite   := cli[i].serverSuite;
         outM.handshakeLog.serverNonce   := cli[i].serverNonce;
         outM.handshakeLog.secretKey     := cli[i].secretKey;
         outM.signKey      := cli[i].verifKey.key;
   
         multisetadd (outM, cliNet);
   
         cli[i].state := M_SERVER_FINISHED;
      else
         -- M_SERVER_ACK_KEY expected
         RunModel := false;
      end;
    end;

  end;
end;

-- Client receives ServerFinished and sends ClientFinished to server

ruleset i: ClientId do
  choose l: cliNet do
    rule 10 "Client receives ServerFinished and sends ClientFinished to server"

       cli[i].state = M_SERVER_FINISHED &
       cliNet[l].dest = i &
       multisetcount(l:serNet, true) < NetworkSize &
       RunModel

    ==>

    var
      inM:  Message;  -- incoming message
      outM: Message;  -- outgoing message
    
    begin
      inM := cliNet[l];
      multisetremove(l, cliNet);

      if inM.mType = M_SERVER_FINISHED then

         -- Decrypt
         if keyEqual(inM.encKey, cli[i].secretKey) then

            -- Check handshake log consistency
            if (ClientLogCheckInFinished ->
                (inM.handshakeLog.session       = cli[i].session) &
                (inM.handshakeLog.clientVersion = cli[i].version) &
                plainEqual(inM.handshakeLog.clientSuite, cli[i].suite) &
                (UseClientNonces ->
                (inM.handshakeLog.clientNonce   = cli[i].nonce)) &
                (inM.handshakeLog.serverVersion = cli[i].serverVersion) &      
                plainEqual(inM.handshakeLog.serverSuite, cli[i].serverSuite) &
                (UseServerNonces ->
                (inM.handshakeLog.serverNonce   = cli[i].serverNonce)) &
                -- (inM.handshakeLog.serverSender  = cli[i].server) &

                -- If this is a resumed session,
                -- only verify contents of M_CLIENT_HELLO_RESUME

                (!cli[i].resumeSession ->
                keyEqual(inM.handshakeLog.secretKey, cli[i].secretKey))) then

               undefine outM;
               outM.source       := i;
               outM.dest         := cli[i].server;
               outM.session      := cli[i].session;
               outM.fromIntruder := false;
               outM.mType        := M_CLIENT_FINISHED;

               -- Log of previous handshake messages
               outM.handshakeLog.session       := cli[i].session;
               outM.handshakeLog.clientVersion := cli[i].version;
               outM.handshakeLog.clientSuite   := cli[i].suite;
               outM.handshakeLog.clientNonce   := cli[i].nonce;
               outM.handshakeLog.serverVersion := cli[i].serverVersion;
               outM.handshakeLog.serverSuite   := cli[i].serverSuite;
               outM.handshakeLog.serverNonce   := cli[i].serverNonce;
               -- outM.handshakeLog.clientSender  := i;
               outM.handshakeLog.secretKey     := cli[i].secretKey;
               outM.encKey       := cli[i].secretKey;
     
               multisetadd (outM, cliNet);
      
               cli[i].state := M_DONE;
           
            else
               -- Handshake log inconsistency
               RunModel := false;
            end;
         else
            -- Client cannot decrypt M_SERVER_FINISHED
            RunModel := false;
         end;
      else
         -- M_SERVER_FINISHED expected
         RunModel := false;
      end;
    end;

  end;
end;

-- SSL2: client receives server's ack and sends ClientFinished to server

ruleset i: ClientId do
  choose l: cliNet do
    rule 10 "SSL2: client receives server's key exchange ack and sends encrypted server nonce (ClientFinished) to server"

       cli[i].state = M_SERVER_ACK_KEY &
       cliNet[l].dest = i &
       RunModel &
       multisetcount(l:serNet, true) < NetworkSize &
       cli[i].serverVersion != MaxVersion

    ==>

    var
      inM:  Message;  -- incoming message
      outM: Message;  -- outgoing message
    
    begin
      inM := cliNet[l];
      multisetremove(l, cliNet);

      if inM.mType = M_SERVER_ACK_KEY then

         undefine outM;
         outM.source       := i;
         outM.dest         := cli[i].server;
         outM.session      := cli[i].session;
         outM.fromIntruder := false;
         outM.mType        := M_2_CLIENT_FINISHED;

         outM.nonce        := cli[i].serverNonce;
         outM.encKey       := cli[i].secretKey;
   
         multisetadd (outM, cliNet);
   
         if ClientAuthenticationInSSL2 then
            cli[i].state := M_2_SERVER_CERTIFICATE_REQUEST;
         else
            cli[i].state := M_2_SERVER_FINISHED;
         end;

      else
         -- M_SERVER_ACK_KEY expected
         RunModel := false;
      end;
    end;

  end;
end;

-- SSL2: client receives request for certificate and sends it
-- to the server

ruleset i: ClientId do
  choose l: cliNet do
    rule 10 "SSL2: client receives CertificateRequest and sends certificate and signed challenge (ClientCertificate) to server"

      cli[i].state = M_2_SERVER_CERTIFICATE_REQUEST &
      cliNet[l].dest = i &
      multisetcount(l:serNet, true) < NetworkSize &
      RunModel

    ==>

    var
      inM:        Message;  	-- incoming message
      outM:       Message;  	-- outgoing message
      challenge:  Nonce; 	-- server challenge
    
    begin
      inM := cliNet[l];
      multisetremove(l, cliNet);
  
      if inM.mType = M_2_SERVER_CERTIFICATE_REQUEST then

         -- Decrypt
         if keyEqual(inM.encKey, cli[i].secretKey) then

            -- Extract challenge
            challenge := inM.nonce;

            -- Send signed challenge back
            undefine outM;
            outM.source       := i;
            outM.dest         := cli[i].server;
            outM.session      := cli[i].session;
            outM.fromIntruder := false;
            outM.mType        := M_2_CLIENT_CERTIFICATE;
   
            outM.verifKey     := cli[i].verifKey;
            outM.nonce        := challenge;
            outM.signKey      := cli[i].verifKey.key;
            outM.encKey       := cli[i].secretKey;
      
            multisetadd (outM, cliNet);
     
            cli[i].state := M_2_SERVER_FINISHED;
  
         else
            -- Client cannot decrypt M_2_SERVER_CERTIFICATE_REQUEST
            RunModel := false;
         end;
      else
         -- M_2_SERVER_CERTIFICATE_REQUEST expected
         RunModel := false;
      end;
    end;

  end;
end;

-- SSL2: client receives ServerFinished

ruleset i: ClientId do
  choose l: cliNet do
    rule 10 "SSL2: client receives ServerFinished"

      cli[i].state = M_2_SERVER_FINISHED &
      cliNet[l].dest = i &
      multisetcount(l:serNet, true) < NetworkSize &
      RunModel

    ==>

    var
      inM:  Message;  -- incoming message
    
    begin
      inM := cliNet[l];
      multisetremove(l, cliNet);
  
      if inM.mType = M_2_SERVER_FINISHED then

         -- Decrypt
         if keyEqual(inM.encKey, cli[i].secretKey) then

            -- Check ServerFinished
            if (inM.nonce      = cli[i].nonce) &
               (inM.encSession = cli[i].session) then

               cli[i].state := M_DONE;
  
            else
               -- Inconsistent ServerFinished
               RunModel := false;
            end;
         else
            -- Client cannot decrypt M_2_SERVER_FINISHED
            RunModel := false;
         end;
      else
         -- M_2_SERVER_FINISHED expected
         RunModel := false;
      end;
    end;

  end;
end;


--
-- Servers
--


-- Server receives ClientHello (new) and sends ServerHello back

ruleset i: ServerId do
  choose l: serNet do
    rule 20 "Server receives ClientHello (new) and sends ServerHello back"

      ser[i].clients[0].state = M_CLIENT_HELLO &
      serNet[l].dest = i &
      serNet[l].session = 0 &
      multisetcount(l:cliNet, true) < NetworkSize &
      RunModel

    ==>

    var
      inM:  Message;   -- incoming message
      outM: Message;   -- outgoing message
      session: SessionId;
    
    begin

      inM := serNet[l];
      multisetremove(l, serNet);

      if inM.mType = M_CLIENT_HELLO then

         session := freshSessionId();

         alias cli: ser[i].clients[session] do

           if (session != 0) then

              -- Haven't run out of sessions!

              cli.client        := inM.source;
              cli.clientVersion := inM.version;
              cli.clientSuite   := inM.suite;
              cli.clientNonce   := inM.nonce;
              cli.resumeSession := false;
              cli.nonce         := freshNonce();
   
              undefine outM;
              outM.source       := i;
              outM.dest         := cli.client;
              outM.session      := session;
              outM.fromIntruder := false;
              outM.mType        := M_SERVER_HELLO;
              outM.version      := ser[i].version;
              outM.suite        := ser[i].suite;
              outM.nonce        := cli.nonce;
        
              cli.state := M_SERVER_SEND_KEY;
   
              multisetadd (outM, serNet);

           else
              -- Ran out of sessions
              RunModel := false;
           end;
         end;
      else
         -- Not a new ClientHello
         RunModel := false;
      end;
    end;

  end;
end;

-- Server receives ClientHello (resume) and sends ServerHello back

ruleset i: ServerId do
  choose l: serNet do
    rule 20 "Server receives ClientHello (resume) and sends ServerHello back"

      ser[i].clients[serNet[l].session].state = M_CLIENT_HELLO_RESUME &
      serNet[l].dest = i &
      multisetcount(l:cliNet, true) < NetworkSize &
      RunModel

    ==>

    var
      inM:  Message;   -- incoming message
      outM: Message;   -- outgoing message
      session: ValidSessionId;
    
    begin

      inM := serNet[l];
      multisetremove(l, serNet);

      if inM.mType = M_CLIENT_HELLO_RESUME then

         session := inM.session;
         alias cli: ser[i].clients[session] do

           -- These may not be needed
           cli.clientVersion := inM.version;
           cli.clientSuite   := inM.suite;
           --
           cli.clientNonce   := inM.nonce;
           cli.resumeSession := true;
           cli.nonce         := freshNonce();

           undefine outM;
           outM.source       := i;
           outM.dest         := cli.client;
           outM.session      := session;
           outM.fromIntruder := false;
           outM.mType        := M_SERVER_HELLO;
           outM.version      := ser[i].version;
           outM.suite        := ser[i].suite;
           outM.nonce        := cli.nonce;
        
	   if cli.clientVersion = MaxVersion then
              
              -- SSL 3.0

              cli.state := M_SERVER_SEND_FINISHED;

           else

              -- SSL 2.0

              cli.state := M_2_CLIENT_FINISHED;

           end;

           multisetadd (outM, serNet);

         end;
      else
         -- M_CLIENT_HELLO_RESUME expected
         RunModel := false;
      end;
    end;

  end;
end;

-- Server sends ServerKeyExchange to client

ruleset i: ServerId do
  ruleset s: ValidSessionId do
    rule 20 "Server sends its public key (ServerKeyExchange) to client"

      ser[i].clients[s].state = M_SERVER_SEND_KEY &
      multisetcount(l:serNet, true) < NetworkSize &
      multisetcount(l:cliNet, true) < NetworkSize &
      RunModel

    ==>

    var
      outM: Message;   -- outgoing message
      session: ValidSessionId;
    
    begin
      alias cli: ser[i].clients[s] do

        undefine outM;
        outM.source       := i;
        outM.dest         := cli.client;
        outM.session      := s;
        outM.fromIntruder := false;
        outM.mType        := M_SERVER_KEY_EXCHANGE;
        outM.publicKey    := ser[i].publicKey;
        outM.verifKey     := ser[i].verifKey;
        outM.signKey      := ser[i].verifKey.key;
     
        cli.state := M_CLIENT_KEY_EXCHANGE;

        multisetadd (outM, serNet);

      end;
    end;

  end;
end;

-- Server receives ClientKeyExchange and sends ack to client

ruleset i: ServerId do
  choose l: serNet do
    rule 20 "Server receives encrypted secret (ClientKeyExchange) and sends ack to client"

      ser[i].clients[serNet[l].session].state = M_CLIENT_KEY_EXCHANGE &
      serNet[l].dest = i &
      multisetcount(l:cliNet, true) < NetworkSize &
      RunModel

    ==>

    var
      inM:  Message;  -- incoming message
      outM: Message;  -- outgoing message
    
    begin
      alias cli: ser[i].clients[serNet[l].session] do

        inM := serNet[l];
        multisetremove(l, serNet);
  
        if inM.mType = M_CLIENT_KEY_EXCHANGE then
  
           -- Decrypt
           if keyEqual(inM.encKey, ser[i].publicKey.key) then
  
              -- Check version consistency
              if (ServerVersionCheckInKey -> 
                  inM.version = cli.clientVersion) then
        
                 cli.secretKey := inM.secretKey;
           
                 undefine outM;
                 outM.source       := i;
                 outM.dest         := cli.client;
                 outM.session      := inM.session;
                 outM.fromIntruder := false;
                 outM.mType        := M_SERVER_ACK_KEY;
           
                 multisetadd (outM, serNet);
           
                 if cli.clientVersion = MaxVersion then

		    -- SSL 3.0

                    cli.state := M_CLIENT_VERIFY;

                 else

		    -- SSL 2.0

                    cli.state := M_2_CLIENT_FINISHED;

                 end;
  
              else
                 -- Client version mismatch
                 RunModel := false;
              end;
           else
              -- Cannot decrypt M_CLIENT_KEY_EXCHANGE
              RunModel := false;
           end;
        else
           -- M_CLIENT_KEY_EXCHANGE expected
           RunModel := false;
        end;

      end;
    end;

  end;
end;

-- Server sends ServerFinished to client

ruleset i: ServerId do
  ruleset s: ValidSessionId do
    rule 20 "Server sends ServerFinished to client"

      ser[i].clients[s].state = M_SERVER_SEND_FINISHED &
      multisetcount(l:serNet, true) < NetworkSize &
      multisetcount(l:cliNet, true) < NetworkSize &
      RunModel

    ==>

    var
      outM: Message;  -- outgoing message
    
    begin
      alias cli: ser[i].clients[s] do

        undefine outM;
        outM.source       := i;
        outM.dest         := cli.client;
        outM.session      := s;
        outM.fromIntruder := false;
        outM.mType        := M_SERVER_FINISHED;

        -- Need to hash only contents of Hello messages
        outM.handshakeLog.session       := s;
        outM.handshakeLog.clientVersion := cli.clientVersion;
        outM.handshakeLog.clientSuite   := cli.clientSuite;
        outM.handshakeLog.clientNonce   := cli.clientNonce;
        outM.handshakeLog.serverVersion := ser[i].version;
        outM.handshakeLog.serverSuite   := ser[i].suite;
        outM.handshakeLog.serverNonce   := cli.nonce;
        -- outM.handshakeLog.serverSender  := i;
        -- Hash secretKey anyway to make all logs look the same
        outM.handshakeLog.secretKey     := cli.secretKey;
        outM.encKey       := cli.secretKey;
              
        multisetadd (outM, serNet);

        cli.state := M_CLIENT_FINISHED;

      end;
    end;

  end;
end;

-- Server receives CertificateVerify and sends ServerFinished to client

ruleset i: ServerId do
  choose l: serNet do
    rule 20 "Server receives signed hash of previous messages (CertificateVerify) and sends ServerFinished to client"

      ser[i].clients[serNet[l].session].state = M_CLIENT_VERIFY &
      serNet[l].dest = i &
      multisetcount(l:cliNet, true) < NetworkSize &
      RunModel

    ==>

    var
      inM:  Message;  -- incoming message
      outM: Message;  -- outgoing message
    
    begin
      alias cli: ser[i].clients[serNet[l].session] do

        inM := serNet[l];
        multisetremove(l, serNet);
  
        if inM.mType = M_CLIENT_VERIFY then

           -- Check certificate for client's verification key
           if (ClientCertificateCheck ->
                  keyEqual(inM.verifKey.key, inM.verifKey.cert.key) &
                  (cli.client = inM.verifKey.cert.owner) &
                  keyEqual(ser[i].authKey, inM.verifKey.cert.signKey)) then

              cli.clientVerifKey := inM.verifKey;
     
              -- Check signature
              if (ClientSignatureCheck ->
                  keyEqual(cli.clientVerifKey.key, inM.signKey)) then
     
                 -- Check handshake log consistency
                 if (ServerKeyCheckInVerify ->
                    keyEqual(inM.handshakeLog.secretKey, cli.secretKey)) &

                    (ServerLogCheckInVerify ->
                    (inM.handshakeLog.session       = inM.session) &
                    (inM.handshakeLog.clientVersion = cli.clientVersion) &
                    plainEqual(inM.handshakeLog.clientSuite, cli.clientSuite) &
                    (UseClientNonces ->
                    (inM.handshakeLog.clientNonce   = cli.clientNonce)) &
                    (inM.handshakeLog.serverVersion = ser[i].version) &
                    plainEqual(inM.handshakeLog.serverSuite, ser[i].suite) &
                    (UseServerNonces ->
                    (inM.handshakeLog.serverNonce   = cli.nonce)) &
                    keyEqual(inM.handshakeLog.secretKey, cli.secretKey)) then

                    if cli.clientVersion = MaxVersion then

                       undefine outM;
                       outM.source       := i;
                       outM.dest         := cli.client;
                       outM.session      := inM.session;
                       outM.fromIntruder := false;
                       outM.mType        := M_SERVER_FINISHED;
   
                       outM.handshakeLog.session       := inM.session;
                       outM.handshakeLog.clientVersion := cli.clientVersion;
                       outM.handshakeLog.clientSuite   := cli.clientSuite;
                       outM.handshakeLog.clientNonce   := cli.clientNonce;
                       outM.handshakeLog.serverVersion := ser[i].version;
                       outM.handshakeLog.serverSuite   := ser[i].suite;
                       outM.handshakeLog.serverNonce   := cli.nonce;
                       outM.handshakeLog.secretKey     := cli.secretKey;
                       -- outM.handshakeLog.serverSender  := i;
                       outM.encKey       := cli.secretKey;
                    
                       multisetadd (outM, serNet);
                    
                       cli.state := M_CLIENT_FINISHED;

                    else
                       cli.state := M_DONE;
                    end;
     
                 else
                    -- Handshake log inconsistency
                    RunModel := false;
                 end;
              else
                 -- Cannot verify the signature
                 RunModel := false;
              end;
           else
              -- Invalid certificate for client's verification key
              RunModel := false;
           end;
        else
           -- M_CLIENT_VERIFY expected
           RunModel := false;
        end;
      end;
    end;

  end;
end;

-- Server receives ClientFinished

ruleset i: ServerId do
  choose l: serNet do
    rule 20 "Server receives ClientFinished"

      ser[i].clients[serNet[l].session].state = M_CLIENT_FINISHED &
      serNet[l].dest = i &
      multisetcount(l:cliNet, true) < NetworkSize &
      RunModel

    ==>

    var
      inM:  Message;  -- incoming message
    
    begin
      alias cli: ser[i].clients[serNet[l].session] do

        inM := serNet[l];
        multisetremove(l, serNet);
  
        if inM.mType = M_CLIENT_FINISHED then

           -- Decrypt
           if keyEqual(inM.encKey, cli.secretKey) then

              -- Check handshake log consistency
              if (ServerLogCheckInFinished ->
                  (inM.handshakeLog.session       = inM.session) &
                  (inM.handshakeLog.clientVersion = cli.clientVersion) &
                  plainEqual(inM.handshakeLog.clientSuite, cli.clientSuite) &
                  (UseClientNonces ->
                  (inM.handshakeLog.clientNonce   = cli.clientNonce)) &
                  (inM.handshakeLog.serverVersion = ser[i].version) &
                  plainEqual(inM.handshakeLog.serverSuite, ser[i].suite) &
                  (UseServerNonces ->
                  (inM.handshakeLog.serverNonce   = cli.nonce)) &
                  -- (inM.handshakeLog.clientSender  = cli.client) &

                  -- If this is a resumed session,
                  -- only verify contents of M_CLIENT_HELLO_RESUME

                  (!cli.resumeSession ->
                   keyEqual(inM.handshakeLog.secretKey, cli.secretKey))) then

                 cli.state := M_DONE;
  
              else
                 -- Handshake log inconsistency
                 RunModel := false;
              end;
           else
              -- Server cannot decrypt M_CLIENT_FINISHED
              RunModel := false;
           end;
        else
           -- M_CLIENT_FINISHED expected
           RunModel := false;
        end;

      end;
    end;

  end;
end;

-- SSL2: server receives ClientFinished and sends CertificateRequest to client
-- (client authentication)

ruleset i: ServerId do
  choose l: serNet do
    rule 20 "SSL2: Server receives ClientFinished and sends CertificateRequest to client"

      ser[i].clients[serNet[l].session].state = M_2_CLIENT_FINISHED &
      serNet[l].dest = i &
      ClientAuthenticationInSSL2 &
      multisetcount(l:cliNet, true) < NetworkSize &
      RunModel

    ==>

    var
      inM:  Message;  -- incoming message
      outM: Message;  -- outgoing message
    
    begin
      alias cli: ser[i].clients[serNet[l].session] do

        inM := serNet[l];
        multisetremove(l, serNet);
  
        if inM.mType = M_2_CLIENT_FINISHED then
  
           -- Decrypt
           if keyEqual(inM.encKey, cli.secretKey) then
  
              -- Check ClientFinished
              if (inM.nonce = cli.nonce) then

                 undefine outM;
                 outM.source       := i;
                 outM.dest         := cli.client;
                 outM.session      := inM.session;
                 outM.fromIntruder := false;
                 outM.mType        := M_2_SERVER_CERTIFICATE_REQUEST;
  
                 cli.challenge     := freshNonce();
		 outM.nonce	   := cli.challenge;
                 outM.encKey       := cli.secretKey;
       
                 multisetadd (outM, serNet);
        
                 cli.state := M_2_CLIENT_CERTIFICATE;
             
              else
                 -- Inconsistent ClientFinished
                 RunModel := false;
              end;
           else
              -- Server cannot decrypt M_2_CLIENT_FINISHED
              RunModel := false;
           end;
        else
           -- M_2_CLIENT_FINISHED expected
           RunModel := false;
        end;
      end;

    end;

  end;
end;

-- SSL2: Server receives ClientCertificate and sends ServerFinished to client
-- (client authentication)

ruleset i: ServerId do
  choose l: serNet do
    rule 20 "SSL2: server receives certificate and signed challenge (ClientCertificate) and sends ServerFinished back"

      ser[i].clients[serNet[l].session].state = M_2_CLIENT_CERTIFICATE &
      serNet[l].dest = i &
      multisetcount(l:cliNet, true) < NetworkSize &
      RunModel

    ==>

    var
      inM:  Message;  -- incoming message
      outM: Message;  -- outgoing message
    
    begin
      alias cli: ser[i].clients[serNet[l].session] do

        inM := serNet[l];
        multisetremove(l, serNet);
  
        if inM.mType = M_2_CLIENT_CERTIFICATE then

           -- Decrypt
           if keyEqual(inM.encKey, cli.secretKey) then

              -- Check certificate for client's verification key
              if (ClientCertificateCheck ->
                     keyEqual(inM.verifKey.key, inM.verifKey.cert.key) &
                     (cli.client = inM.verifKey.cert.owner) &
                     keyEqual(ser[i].authKey, inM.verifKey.cert.signKey)) then

                 cli.clientVerifKey := inM.verifKey;
     
                 -- Check signature
                 if (ClientSignatureCheck ->
                    keyEqual(cli.clientVerifKey.key, inM.signKey)) then
     
                    -- Check challenge
                    if (inM.nonce = cli.challenge) then

                       undefine outM;
                       outM.source       := i;
                       outM.dest         := cli.client;
                       outM.session      := inM.session;
                       outM.fromIntruder := false;
                       outM.mType        := M_2_SERVER_FINISHED;
        
      		       outM.nonce	 := cli.clientNonce;
                       outM.encSession   := inM.session;
                       outM.encKey       := cli.secretKey;
             
                       multisetadd (outM, serNet);
              
                       cli.state := M_DONE;
     
                    else
                       -- Wrong challenge
                       RunModel := false;
                    end;
                 else
                    -- Cannot verify the signature
                    RunModel := false;
                 end;
              else
                 -- Invalid certificate for client's verification key
                 RunModel := false;
              end;
           else
              -- Cannot decrypt M_2_CLIENT_CERTIFICATE
              RunModel := false;
           end;
        else
           -- M_2_CLIENT_CERTIFICATE expected
           RunModel := false;
        end;
      end;
    end;

  end;
end;

-- SSL2: server receives ClientFinished and sends ServerFinished to client
-- (no client authentication)

ruleset i: ServerId do
  choose l: serNet do
    rule 20 "SSL2: Server receives ClientFinished and sends ServerFinished to client"

      ser[i].clients[serNet[l].session].state = M_2_CLIENT_FINISHED &
      serNet[l].dest = i &
      !ClientAuthenticationInSSL2 &
      multisetcount(l:cliNet, true) < NetworkSize &
      RunModel

    ==>

    var
      inM:  Message;  -- incoming message
      outM: Message;  -- outgoing message
    
    begin
      alias cli: ser[i].clients[serNet[l].session] do

        inM := serNet[l];
        multisetremove(l, serNet);
  
        if inM.mType = M_2_CLIENT_FINISHED then
  
           -- Decrypt
           if keyEqual(inM.encKey, cli.secretKey) then
  
              -- Check ClientFinished
              if (inM.nonce = cli.nonce) then

                 undefine outM;
                 outM.source       := i;
                 outM.dest         := cli.client;
                 outM.session      := inM.session;
                 outM.fromIntruder := false;
                 outM.mType        := M_2_SERVER_FINISHED;
  
		 outM.nonce	   := cli.clientNonce;
                 outM.encSession   := inM.session;
                 outM.encKey       := cli.secretKey;
       
                 multisetadd (outM, serNet);
        
                 cli.state := M_DONE;
             
              else
                 -- Inconsistent ClientFinished
                 RunModel := false;
              end;
           else
              -- Server cannot decrypt M_2_CLIENT_FINISHED
              RunModel := false;
           end;
        else
           -- M_2_CLIENT_FINISHED expected
           RunModel := false;
        end;
      end;

    end;

  end;
end;


--
-- Switch to another run
--


ruleset i: ClientId do
  ruleset resumeSession: boolean do
    rule 10 "Start a new run"
  
       ismember(cli[i].server, ServerId) &
       cli[i].state = M_DONE &
       ser[cli[i].server].clients[cli[i].session].state = M_DONE &
       runCount[i] > 0 &
       RunModel        
  
    ==>
  
    begin
      alias s: cli[i].session do
  
        cli[i].state := M_SLEEP;
        if (resumeSession = true) then
           ser[cli[i].server].clients[s].state := M_CLIENT_HELLO_RESUME;
           cli[i].resumeSession := true;
        else
           ser[cli[i].server].clients[s].state := M_SLEEP;
           cli[i].resumeSession := false;
           cli[i].session := 0;
           undefine cli[i].server;

           -- nextSession := 0;
        end;
  
        runCount[i] := runCount[i] - 1;
      end;
    end;

  end;
end;


--
-- Intruders
--


-- Intruder intercepts a message

ruleset i: IntruderId do
  choose l: cliNet do
    rule 5 "Intruder intercepts client's message"

      cliNet[l].fromIntruder = false &
      RunModel

    ==>

    var
      recordMsg: boolean;
    begin
      alias msg: cliNet[l] do   -- message from the net

        recordMsg := false;

        -- learn a nonce
        if msg.mType = M_CLIENT_HELLO |
           msg.mType = M_CLIENT_HELLO_RESUME then
           alias nonces: int[i].nonces do
             if multisetcount(n: nonces,
                nonces[n] = msg.nonce) = 0 then
                multisetadd(msg.nonce, nonces);
             end;
           end;
        end;

        -- decrypt (if possible) and learn shared secret
        if msg.mType = M_CLIENT_KEY_EXCHANGE then
           if keyEqual(msg.encKey, int[i].publicKey.key) then
              alias sKeys: int[i].secretKeys do
                if multisetcount(s: sKeys,
                   keyEqual(sKeys[s], msg.secretKey)) = 0 then
                   multisetadd(msg.secretKey, sKeys);
                end;
              end;
           else
              -- If cannot decrypt, record
              recordMsg := true;
           end;
        end;

        -- learn client's verification key and handshake log
        if msg.mType = M_CLIENT_VERIFY then
           alias vKeys: int[i].verifKeys do
             if multisetcount(v: vKeys,
                certKeyEqual(vKeys[v], msg.verifKey)) = 0 then
                multisetadd(msg.verifKey, vKeys);
             end;
           end;
           alias hLogs: int[i].logs do
             if multisetcount(l: hLogs,
                logEqual(hLogs[l], msg.handshakeLog)) = 0 then
                multisetadd(msg.handshakeLog, hLogs);
             end;
           end;

           -- Signed => cannot reproduce it
           recordMsg := true;
        end;

        -- decrypt (if possible) and learn handshake log
        if msg.mType = M_CLIENT_FINISHED then
           alias sKeys: int[i].secretKeys do
             alias hLogs: int[i].logs do
               if multisetcount(s: sKeys,
                  keyEqual(sKeys[s], msg.encKey)) > 0 then
                  -- Can decrypt
                  if multisetcount(l: hLogs,
                     logEqual(hLogs[l], msg.handshakeLog)) = 0 then
                     multisetadd(msg.handshakeLog, hLogs);
                  end;
               else
                 -- If cannot decrypt, record
                 recordMsg := true;
               end;
             end;
           end;
        end;

	-- All information in SSL2 ClientFinished is public (nonce).
	-- Intruder does not need to decrypt it.
	-- However, it may record the entire message for later replay.
        if msg.mType = M_2_CLIENT_FINISHED then
           recordMsg := true;
        end;

        -- decrypt (if possible) and learn challenge from 
        -- SSL2 client certificate
        if msg.mType = M_2_CLIENT_CERTIFICATE then
           alias sKeys: int[i].secretKeys do
             alias vKeys: int[i].verifKeys do
             alias nonces: int[i].nonces do
               if multisetcount(s: sKeys,
                  keyEqual(sKeys[s], msg.encKey)) > 0 then
                  -- Can decrypt
		  -- Learn verification key
                  if multisetcount(v: vKeys,
                     certKeyEqual(vKeys[v], msg.verifKey)) = 0 then
                     multisetadd(msg.verifKey, vKeys);
                  end;
                  -- Learn nonce
                  if multisetcount(n: nonces,
                     (nonces[n] = msg.nonce)) = 0 then
                     multisetadd(msg.nonce, nonces);
                  end;
                  -- Record the entire message for replay
                  -- under different encryption
                  alias certs: int[i].clientCerts do
                    if multisetcount(c: certs,
                       msgEqual(certs[c], msg)) = 0 then
                       multisetadd(msg, certs);
                    end;
                  end;
               else
                 -- If cannot decrypt, record
                 recordMsg := true;
               end;
             end;
             end;
           end;
        end;

        -- record the message, if cannot reproduce it
        if recordMsg = true then
           alias known: int[i].messages do
             if multisetcount(m: known,
                msgEqual(known[m], msg)) = 0 then
                multisetadd(msg, known);
             end;
           end;
        end;

        multisetremove(l, cliNet);

      end;  -- alias msg
    end;  -- begin
    
  end;
end;

ruleset i: IntruderId do
  choose l: serNet do
    rule 5 "Intruder intercepts server's message"

      serNet[l].fromIntruder = false &
      RunModel

    ==>

    var
      recordMsg: boolean;
    begin
      alias msg: serNet[l] do   -- message from the net

        recordMsg := false;

        -- learn nonce
        if msg.mType = M_SERVER_HELLO then
           alias nonces: int[i].nonces do
             if multisetcount(n: nonces,
                nonces[n] = msg.nonce) = 0 then
                multisetadd(msg.nonce, nonces);
             end;
           end;
        end;

        -- learn server's public key and verification key
        if msg.mType = M_SERVER_KEY_EXCHANGE then         
           alias sKeys: int[i].publicKeys do
             if multisetcount(s: sKeys,
                certKeyEqual(sKeys[s], msg.publicKey)) = 0 then
                multisetadd(msg.publicKey, sKeys);
             end;
           end;
           alias vKeys: int[i].verifKeys do
             if multisetcount(v: vKeys,
                certKeyEqual(vKeys[v], msg.verifKey)) = 0 then
                multisetadd(msg.verifKey, vKeys);
             end;
           end;

           -- Signed => cannot reproduce it
           recordMsg := true;
        end;

        -- decrypt (if possible) and learn handshake log
        if msg.mType = M_SERVER_FINISHED then
           alias sKeys: int[i].secretKeys do
             alias hLogs: int[i].logs do
               if multisetcount(s: sKeys,
                  keyEqual(sKeys[s], msg.encKey)) > 0 then
                  -- Can decrypt
                  if multisetcount(l: hLogs,
                     logEqual(hLogs[l], msg.handshakeLog)) = 0 then
                     multisetadd(msg.handshakeLog, hLogs);
                  end;
               else
                 -- If cannot decrypt, record
                 recordMsg := true;
               end;
             end;
           end;
        end;

	-- All information in SSL2 ServerFinished is public 
	-- (nonce and encSession).
	-- Intruder does not need to decrypt it.
	-- However, it may record the entire message for later replay.
        if msg.mType = M_2_SERVER_FINISHED then
           recordMsg := true;
        end;

        -- decrypt (if possible) and learn challenge
        if msg.mType = M_2_SERVER_CERTIFICATE_REQUEST then
           alias sKeys: int[i].secretKeys do
             alias nonces: int[i].nonces do
               if multisetcount(s: sKeys,
                  keyEqual(sKeys[s], msg.encKey)) > 0 then
                  -- Can decrypt
                  if multisetcount(n: nonces,
                     (nonces[n] = msg.nonce)) = 0 then
                     multisetadd(msg.nonce, nonces);
                  end;
               else
                 -- If cannot decrypt, record
                 recordMsg := true;
               end;
             end;
           end;
        end;

        -- record the message, if cannot reproduce it
        if recordMsg = true then
           alias known: int[i].messages do
             if multisetcount(m: known,
                msgEqual(known[m], msg)) = 0 then
                multisetadd(msg, known);
             end;
           end;
        end;

        multisetremove(l, serNet);

      end;  -- alias msg
    end;  -- begin
    
  end;
end;

-- Intruder replays a recorded message to server

ruleset i: IntruderId do
  choose m: int[i].messages do
    ruleset s: ValidSessionId do
      ruleset d: ServerId do
        rule 50 "Intruder replays message to server"
    
    	  -- Only send message if the recipient is ready for it
    
          ser[d].clients[s].state = int[i].messages[m].mType &
          multisetcount(l: serNet, true) < NetworkSize &
          multisetcount(l: cliNet, true) < NetworkSize &
          RunModel
        
        ==>
    
        var
          outM: Message;
    
        begin
          outM := int[i].messages[m];
          outM.dest         := d;
          outM.fromIntruder := true;
          -- If this message is under negotiated cipher,
          -- can change session only if the secret key is known.
          if ((outM.mType = M_CLIENT_FINISHED) |
              (outM.mType = M_2_CLIENT_FINISHED) |
              (outM.mType = M_2_CLIENT_CERTIFICATE) ->
              multisetcount(s: int[i].secretKeys, 
                keyEqual(int[i].secretKeys[s], outM.encKey)) > 0) then
             outM.session := s;
          end;

          multisetadd(outM, serNet);
        end;  -- begin
    
      end;
    end;
  end;
end;

-- Intruder replays a recorded message to client

ruleset i: IntruderId do
  choose m: int[i].messages do
    ruleset d: ClientId do
      rule 50 "Intruder replays message to client"
  
  	  -- Only send message if the recipient is ready for it
  
        cli[d].state = int[i].messages[m].mType &
        multisetcount(l: cliNet, true) < NetworkSize &
        multisetcount(l: serNet, true) < NetworkSize &
        RunModel
  
      ==>
  
      var
        outM: Message;
  
      begin
        outM := int[i].messages[m];
        outM.source       := i;
        outM.dest         := d;
        -- Leave session as it is
        outM.fromIntruder := true;

        multisetadd(outM, cliNet);
      end;  -- begin
    
    end;
  end;
end;

-- Intruder generates a ClientHello message (new session)

ruleset i: IntruderId do
  ruleset s: ClientId do
  ruleset d: ServerId do
    choose n: int[i].nonces do
    ruleset versionAttack: boolean do
    ruleset suiteAttack: boolean do
      rule 50 "Intruder generates ClientHello (new session)"
  
        -- Don't start unless there are available sessions
        !NoMoreSessions &
        (ismember(s, ClientId) | 
        (ismember(s, IntruderId) -> IntruderMayInitiate)) &
        multisetcount(l:serNet, true) < NetworkSize &
        multisetcount(l:cliNet, true) < NetworkSize &
        RunModel
  
      ==>
  
      var
        outM: Message;  -- outgoing message
  
      begin
        undefine outM;
        outM.source       := s;
        outM.dest         := d;
        outM.session      := 0;
        outM.fromIntruder := true;
        outM.mType        := M_CLIENT_HELLO;

        if versionAttack then
             outM.version := int[i].evilVersion;
        else outM.version := int[i].goodVersion;
        end;
        if suiteAttack then
             outM.suite   := int[i].evilSuite;
        else outM.suite   := int[i].goodSuite;
        end;
        outM.nonce        := int[i].nonces[n];
  
        multisetadd (outM, serNet);
      end;
  
    end;
    end;
    end;
  end;
  end;
end;

-- Intruder generates a ClientHello message (resumed session)

ruleset i: IntruderId do
  ruleset s: ValidSessionId do
    ruleset d: ServerId do
      choose n: int[i].nonces do
      ruleset versionAttack: boolean do
      ruleset suiteAttack: boolean do
        rule 50 "Intruder generates ClientHello (resumed session)"
    
          ser[d].clients[s].state = M_CLIENT_HELLO_RESUME &
          multisetcount(l:serNet, true) < NetworkSize &
          multisetcount(l:cliNet, true) < NetworkSize &
          RunModel
    
        ==>
    
        var
          outM: Message;  -- outgoing message
    
        begin
          undefine outM;
          outM.source       := i;
          outM.dest         := d;
          outM.session      := s;
          outM.fromIntruder := true;
          outM.mType        := M_CLIENT_HELLO_RESUME;

          if versionAttack then
                outM.version := int[i].evilVersion;
          else  outM.version := int[i].goodVersion;
          end;
          if suiteAttack then
                outM.suite := int[i].evilSuite;
          else  outM.suite := int[i].goodSuite;
          end;
          outM.nonce         := int[i].nonces[n];
    
          multisetadd (outM, serNet);
        end;
    
      end;
      end;
      end;
    end;
  end;
end;

-- Intruder generates a ServerHello message

ruleset i: IntruderId do
  ruleset d: ClientId do
    ruleset s: ValidSessionId do
      choose n: int[i].nonces do
      ruleset versionAttack: boolean do
      ruleset suiteAttack: boolean do
        rule 50 "Intruder generates ServerHello"

          cli[d].state = M_SERVER_HELLO &
          multisetcount(l:cliNet, true) < NetworkSize &
          multisetcount(l:serNet, true) < NetworkSize &
          RunModel
  
        ==>
  
        var
          outM: Message;  -- outgoing message
  
        begin
          undefine outM;
          outM.source       := i;
          outM.dest         := d;
          outM.session      := s;
          outM.fromIntruder := true;
          outM.mType        := M_SERVER_HELLO;

          if versionAttack then
                outM.version := int[i].evilVersion;
          else  outM.version := int[i].goodVersion;
          end;
          if suiteAttack then
                outM.suite := int[i].evilSuite;
          else  outM.suite := int[i].goodSuite;
          end;
          outM.nonce     := int[i].nonces[n];
          
          multisetadd (outM, cliNet);
        end;

      end;
      end;
      end;
    end;
  end;
end;

-- Intruder generates a ServerKeyExchange message with known
-- public and verification keys (possibly its own)

ruleset i: IntruderId do
  ruleset d: ClientId do
    ruleset s: ValidSessionId do
      choose publicKey: int[i].publicKeys do
      choose verifKey: int[i].verifKeys do
        rule 50 "Intruder generates ServerKeyExchange with known public and verification keys"

          cli[d].state = M_SERVER_KEY_EXCHANGE &
          multisetcount(l:cliNet, true) < NetworkSize &
          multisetcount(l:serNet, true) < NetworkSize &
          RunModel
  
        ==>
  
        var
          outM: Message;  -- outgoing message
  
        begin
          undefine outM;
          outM.source       := i;
          outM.dest         := d;
          outM.session      := s;
          outM.fromIntruder := true;
          outM.mType        := M_SERVER_KEY_EXCHANGE;

          outM.publicKey := int[i].publicKeys[publicKey];
          outM.verifKey  := int[i].verifKeys[verifKey];
          -- Intruder can only sign for itself
          outM.signKey   := int[i].verifKey.key;
          
          multisetadd (outM, cliNet);
        end;

      end;
      end;
    end;
  end;
end;

-- Intruder generates a ClientKeyExchange message with 
-- a known secret (possibly its own)

ruleset i: IntruderId do
  ruleset s: ValidSessionId do
    ruleset d: ServerId do
      choose secretKey: int[i].secretKeys do
          rule 50 "Intruder generates ClientKeyExchange with a known secret"
      
            ser[d].clients[s].state = M_CLIENT_KEY_EXCHANGE &
            multisetcount(l:cliNet, true) < NetworkSize &
            multisetcount(l:serNet, true) < NetworkSize &
            RunModel
      
          ==>
      
          var
            outM: Message;  -- outgoing message
      
          begin 
            alias sKeys: int[i].publicKeys do
              -- Only send if can encrypt with the appropriate server key
              if multisetcount(s: sKeys, 
                 keyEqual(sKeys[s].key, ser[d].publicKey.key)) > 0 then
      
                 undefine outM;
                 outM.source       := i;
                 outM.dest         := d;
                 outM.session      := s;
                 outM.fromIntruder := true;
                 outM.mType        := M_CLIENT_KEY_EXCHANGE;

                 -- Insert version # expected by the recipient
                 outM.version   := ser[d].clients[s].clientVersion;
                 outM.secretKey := int[i].secretKeys[secretKey];
                 outM.encKey    := ser[d].publicKey.key;
      
                 multisetadd (outM, serNet);
    
              end;  -- if multisetcount
            end;  -- alias
          end;  -- begin
     
        end;
    end;
  end;
end;

-- Intruder generates an ack to ClientKeyExchange

ruleset i: IntruderId do
  ruleset d: ClientId do
    rule 50 "Intruder generates ack to ClientKeyExchange"
    
      cli[d].state = M_SERVER_ACK_KEY &
      multisetcount(l:cliNet, true) < NetworkSize &
      multisetcount(l:serNet, true) < NetworkSize &
      RunModel
    
    ==>
    
    var
      outM: Message;  -- outgoing message
    
    begin 
      undefine outM;
      outM.source       := i;
      outM.dest         := d;
      outM.session      := cli[d].session;
      outM.fromIntruder := true;
      outM.mType        := M_SERVER_ACK_KEY;
    
      multisetadd (outM, cliNet);
    end;

  end;
end;

-- Intruder generates a CertificateVerify message with 
-- a known verification key (possibly its own) and
-- a handshake log assembled from known information

ruleset i: IntruderId do
  ruleset s: ValidSessionId do
    ruleset d: ServerId do
      choose verifKey: int[i].verifKeys do
        choose n1: int[i].nonces do
        choose n2: int[i].nonces do
        choose secretKey: int[i].secretKeys do
          rule 50 "Intruder generates CertificateVerify with a known verification key (forged log)"
      
            ser[d].clients[s].state = M_CLIENT_VERIFY &
            multisetcount(l:cliNet, true) < NetworkSize &
            multisetcount(l:serNet, true) < NetworkSize &
            RunModel
      
          ==>
      
          var
            outM: Message;  -- outgoing message
      
          begin 
      
            undefine outM;
            outM.source       := i;
            outM.dest         := d;
            outM.session      := s;
            outM.fromIntruder := true;
            outM.mType        := M_CLIENT_VERIFY;

            outM.verifKey := int[i].verifKeys[verifKey];
            -- Forge handshake log
	    -- Use version #s and suites expected by the recipient
            outM.handshakeLog.session       := s;
            outM.handshakeLog.clientVersion := ser[d].clients[s].clientVersion;
            outM.handshakeLog.clientSuite   := ser[d].clients[s].clientSuite;
            outM.handshakeLog.clientNonce   := int[i].nonces[n1];
            outM.handshakeLog.serverVersion := ser[d].version;
            outM.handshakeLog.serverSuite   := ser[d].suite;
            outM.handshakeLog.serverNonce   := int[i].nonces[n2];
            outM.handshakeLog.secretKey     := int[i].secretKeys[secretKey];
            -- Can only sign for itself
            outM.signKey  := int[i].verifKey.key;
      
            multisetadd (outM, serNet);
      
          end;
    
        end;
      end;
      end;
      end;
    end;
  end;
end;

-- Intruder generates a CertificateVerify message with 
-- a known verification key (possibly its own) and
-- intercepted handshake log

ruleset i: IntruderId do
  ruleset s: ValidSessionId do
  ruleset d: ServerId do
    choose verifKey: int[i].verifKeys do
    choose lg: int[i].logs do
      rule 50 "Intruder generates CertificateVerify with a known verification key (intercepted log)"
  
        ser[d].clients[s].state = M_CLIENT_VERIFY &
        multisetcount(l:cliNet, true) < NetworkSize &
        multisetcount(l:serNet, true) < NetworkSize &
        RunModel
  
      ==>
  
      var
        outM: Message;  -- outgoing message
  
      begin 
  
        undefine outM;
        outM.source       := i;
        outM.dest         := d;
        outM.session      := s;
        outM.fromIntruder := true;
        outM.mType        := M_CLIENT_VERIFY;

        outM.verifKey     := int[i].verifKeys[verifKey];
        outM.handshakeLog := int[i].logs[lg];
        -- Can only sign for itself
        outM.signKey      := int[i].verifKey.key;
  
        multisetadd (outM, serNet);
  
      end;

    end;
    end;
  end;
  end;
end;

-- Intruder generates a ServerFinished message with
-- a forged handshake log

ruleset i: IntruderId do
  ruleset d: ClientId do
    choose  n1: int[i].nonces do
    choose  n2: int[i].nonces do
    choose  secretKey: int[i].secretKeys do
    ruleset sender: ServerId do
      rule 50 "Intruder generates ServerFinished (forged log)"
  
        cli[d].state = M_SERVER_FINISHED &
        multisetcount(l:cliNet, true) < NetworkSize &
        multisetcount(l:serNet, true) < NetworkSize &
        RunModel
  
      ==>
  
      var
        outM: Message;  -- outgoing message
  
      begin
        alias sKeys: int[i].secretKeys do
          -- Only send if can encrypt with the appropriate shared secret.
          if multisetcount(s: sKeys, 
             keyEqual(sKeys[s], cli[d].secretKey)) > 0 then
  
             undefine outM;
             outM.source       := i;
             outM.dest         := d;
             outM.session      := cli[d].session;
             outM.fromIntruder := true;
             outM.mType        := M_SERVER_FINISHED;

             -- Forge handshake log
             outM.handshakeLog.session       := cli[d].session;
             outM.handshakeLog.clientVersion := cli[d].version;
             outM.handshakeLog.clientSuite   := cli[d].suite;
             outM.handshakeLog.clientNonce   := int[i].nonces[n1];
             outM.handshakeLog.serverVersion := cli[d].serverVersion;
             outM.handshakeLog.serverSuite   := cli[d].serverSuite;
             outM.handshakeLog.serverNonce   := int[i].nonces[n2];             
             outM.handshakeLog.secretKey     := sKeys[secretKey];
             -- outM.handshakeLog.serverSender  := sender;
             outM.encKey := cli[d].secretKey;
   
             multisetadd (outM, cliNet);
          end;
        end;
      end;
  
    end;
    end;
    end;
    end;
  end;
end;

-- Intruder generates a ServerFinished message with 
-- an intercepted handshake log

ruleset i: IntruderId do
  ruleset d: ClientId do
    choose lg: int[i].logs do
      rule 50 "Intruder generates ServerFinished (intercepted log)"
  
        cli[d].state = M_SERVER_FINISHED &
        multisetcount(l:cliNet, true) < NetworkSize &
        multisetcount(l:serNet, true) < NetworkSize &
        RunModel
  
      ==>
  
      var
        outM: Message;  -- outgoing message
  
      begin
        alias sKeys: int[i].secretKeys do
          -- Only send if can encrypt with the appropriate shared secret.
          if multisetcount(s: sKeys, 
             keyEqual(sKeys[s], cli[d].secretKey)) > 0 then
  
             undefine outM;
             outM.source       := i;
             outM.dest         := d;
             outM.session      := cli[d].session;
             outM.fromIntruder := true;
             outM.mType        := M_SERVER_FINISHED;

             outM.handshakeLog := int[i].logs[lg];
             outM.encKey       := cli[d].secretKey;
   
             multisetadd (outM, cliNet);

          end;
        end;
      end;
  
    end;
  end;
end;

-- Intruder generates a ClientFinished message with 
-- a forged handshake log

ruleset i: IntruderId do
  ruleset s: ValidSessionId do
    ruleset d: ServerId do
      ruleset session: ValidSessionId do
      choose  n1: int[i].nonces do
      choose  n2: int[i].nonces do
      choose  secretKey: int[i].secretKeys do
      ruleset sender: ClientId do
        rule 50 "Intruder generates ClientFinished (forged log)"
    
          ser[d].clients[s].state = M_CLIENT_FINISHED &
          multisetcount(l:cliNet, true) < NetworkSize &
          multisetcount(l:serNet, true) < NetworkSize &
          RunModel
   
        ==>
    
        var
          outM: Message;  -- outgoing message
    
        begin
          alias sKeys: int[i].secretKeys do
            -- Only send if can encrypt with the appropriate shared secret.
            if multisetcount(k: sKeys, 
               keyEqual(sKeys[k], ser[d].clients[s].secretKey)) > 0 then
    
               undefine outM;
               outM.source       := i;
               outM.dest         := d;
               outM.session      := s;
               outM.fromIntruder := true;
               outM.mType        := M_CLIENT_FINISHED;
  
               -- Forge handshake log
               outM.handshakeLog.session       := session;
               outM.handshakeLog.clientVersion := 
                    ser[d].clients[s].clientVersion;
               outM.handshakeLog.clientSuite   := 
                    ser[d].clients[s].clientSuite;
               outM.handshakeLog.clientNonce   := int[i].nonces[n1];
               outM.handshakeLog.serverVersion := ser[d].version;
               outM.handshakeLog.serverSuite   := ser[d].suite;
               outM.handshakeLog.serverNonce   := int[i].nonces[n2];
               outM.handshakeLog.secretKey     := sKeys[secretKey];
               -- outM.handshakeLog.clientSender := sender;

               outM.encKey := ser[d].clients[s].secretKey;

               multisetadd (outM, serNet);

            end;
          end;
        end;
    
      end;
      end;
      end;
      end;
      end;
    end;
  end;
end;

-- Intruder generates a ClientFinished message with
-- an intercepted handshake log

ruleset i: IntruderId do
  ruleset s: ValidSessionId do
    ruleset d: ServerId do
      choose lg: int[i].logs do
        rule 50 "Intruder generates ClientFinished (intercepted log)"
    
          ser[d].clients[s].state = M_CLIENT_FINISHED &
          multisetcount(l:cliNet, true) < NetworkSize &
          multisetcount(l:serNet, true) < NetworkSize &
          RunModel
    
        ==>
    
        var
          outM: Message;  -- outgoing message
    
        begin
          alias sKeys: int[i].secretKeys do
            -- Only send if can encrypt with the appropriate shared secret.
            if multisetcount(k: sKeys, 
               keyEqual(sKeys[k], ser[d].clients[s].secretKey)) > 0 then
    
               undefine outM;
               outM.source       := i;
               outM.dest         := d;
               outM.session      := s;
               outM.fromIntruder := true;
               outM.mType        := M_CLIENT_FINISHED;
  
               outM.handshakeLog := int[i].logs[lg];
               outM.encKey       := ser[d].clients[s].secretKey;
          
               multisetadd (outM, serNet);
            end;
          end;
        end;
    
      end;
    end;
  end;
end;

-- Intruder generates an SSL2 ClientFinished message

ruleset i: IntruderId do
  ruleset s: ValidSessionId do
    ruleset d: ServerId do
      choose n: int[i].nonces do
        rule 50 "Intruder generates SSL2 ClientFinished"
    
          ser[d].clients[s].state = M_2_CLIENT_FINISHED &
          multisetcount(l:cliNet, true) < NetworkSize &
          multisetcount(l:serNet, true) < NetworkSize &
          RunModel
   
        ==>
    
        var
          outM: Message;  -- outgoing message
    
        begin
          alias sKeys: int[i].secretKeys do
            -- Only send if can encrypt with the appropriate shared secret.
            if multisetcount(k: sKeys, 
               keyEqual(sKeys[k], ser[d].clients[s].secretKey)) > 0 then
    
               undefine outM;
               outM.source       := i;
               outM.dest         := d;
               outM.session      := s;
               outM.fromIntruder := true;
               outM.mType        := M_2_CLIENT_FINISHED;
  
               outM.nonce        := int[i].nonces[n];
               outM.encKey       := ser[d].clients[s].secretKey;

               multisetadd (outM, serNet);

            end;
          end;
        end;
    
      end;
    end;
  end;
end;

-- Intruder generates an SSL2 CertificateRequest message

ruleset i: IntruderId do
  ruleset s: ValidSessionId do
    ruleset d: ClientId do
      choose  n: int[i].nonces do
        rule 50 "Intruder generates SSL2 CertificateRequest"
    
          cli[d].state = M_2_SERVER_CERTIFICATE_REQUEST &
          multisetcount(l:cliNet, true) < NetworkSize &
          multisetcount(l:serNet, true) < NetworkSize &
          RunModel
   
        ==>
    
        var
          outM: Message;  -- outgoing message
    
        begin
          alias sKeys: int[i].secretKeys do
            -- Only send if can encrypt with the appropriate shared secret.
            if multisetcount(k: sKeys, 
               keyEqual(sKeys[k], cli[d].secretKey)) > 0 then
    
               undefine outM;
               outM.source       := i;
               outM.dest         := d;
               outM.session      := s;
               outM.fromIntruder := true;
               outM.mType        := M_2_SERVER_CERTIFICATE_REQUEST;
  
               outM.nonce        := int[i].nonces[n];
               outM.encKey       := cli[d].secretKey;

               multisetadd (outM, cliNet);

            end;
          end;
        end;
    
      end;
    end;
  end;
end;

-- Intruder generates an SSL2 ClientCertificate message

ruleset i: IntruderId do
  ruleset s: ValidSessionId do
  ruleset d: ServerId do
    choose  verifKey: int[i].verifKeys do
    choose  n: int[i].nonces do
      rule 50 "Intruder generates SSL2 ClientCertificate"
  
        ser[d].clients[s].state = M_2_CLIENT_CERTIFICATE &
        multisetcount(l:cliNet, true) < NetworkSize &
        multisetcount(l:serNet, true) < NetworkSize &
        RunModel
  
      ==>
  
      var
        outM: Message;  -- outgoing message
  
      begin
        alias sKeys: int[i].secretKeys do
          -- Only send if can encrypt with the appropriate shared secret.
          if multisetcount(k: sKeys, 
             keyEqual(sKeys[k], ser[d].clients[s].secretKey)) > 0 then
  
             undefine outM;
             outM.source       := i;
             outM.dest         := d;
             outM.session      := s;
             outM.fromIntruder := true;
             outM.mType        := M_2_CLIENT_CERTIFICATE;
     
             outM.verifKey     := int[i].verifKeys[verifKey];
             outM.nonce        := int[i].nonces[n];
             -- Can only sign for itself
             outM.signKey      := int[i].verifKey.key;
             outM.encKey       := ser[d].clients[s].secretKey;
       
             multisetadd (outM, serNet);

          end;
        end;
      end;

    end;
    end;
  end;
  end;
end;

-- Intruder replays an SSL2 ClientCertificate message 
-- under different encryption

ruleset i: IntruderId do
  choose m: int[i].clientCerts do
    ruleset s: ValidSessionId do
      ruleset d: ServerId do
        rule 50 "Intruder replays SSL2 client certificate"
    
          ser[d].clients[s].state = M_2_CLIENT_CERTIFICATE &
          multisetcount(l: serNet, true) < NetworkSize &
          multisetcount(l: cliNet, true) < NetworkSize &
          RunModel
        
        ==>
    
        var
          outM: Message;
    
        begin
          alias sKeys: int[i].secretKeys do
            -- Only send if can encrypt with the appropriate shared secret.
            if multisetcount(k: sKeys, 
               keyEqual(sKeys[k], ser[d].clients[s].secretKey)) > 0 then

               outM := int[i].clientCerts[m];
               outM.dest         := d;
               outM.session      := s;
               outM.fromIntruder := true;

               outM.encKey       := ser[d].clients[s].secretKey;

               multisetadd(outM, serNet);

            end;
          end;

        end;  -- begin
    
      end;
    end;
  end;
end;

-- Intruder generates an SSL2 ServerFinished message

ruleset i: IntruderId do
  ruleset s: ValidSessionId do
    ruleset d: ClientId do
      choose  n: int[i].nonces do
      ruleset session: ValidSessionId do
        rule 50 "Intruder generates SSL2 ServerFinished"
    
          cli[d].state = M_2_SERVER_FINISHED &
          multisetcount(l:cliNet, true) < NetworkSize &
          multisetcount(l:serNet, true) < NetworkSize &
          RunModel
   
        ==>
    
        var
          outM: Message;  -- outgoing message
    
        begin
          alias sKeys: int[i].secretKeys do
            -- Only send if can encrypt with the appropriate shared secret.
            if multisetcount(k: sKeys, 
               keyEqual(sKeys[k], cli[d].secretKey)) > 0 then
    
               undefine outM;
               outM.source       := i;
               outM.dest         := d;
               outM.session      := s;
               outM.fromIntruder := true;
               outM.mType        := M_2_SERVER_FINISHED;
  
               outM.nonce        := int[i].nonces[n];
               outM.encSession   := session;
               outM.encKey       := cli[d].secretKey;

               multisetadd (outM, cliNet);

            end;
          end;
        end;
    
      end;
      end;
    end;
  end;
end;


--
-- Start state
--


startstate
var 
   nonce:	Nonce;
   publicKey:	CertifiedKey;
   verifKey:	CertifiedKey;
   secretKey:	Key;
   authKey:	Key;
begin

  -- Initialize run count, nonce and session id generators
  for i: ClientId do
      runCount[i] := MaxRepeatRuns;
  end;
  SessionBound   := MaxSessionId;
  RunModel       := true;
  NoMoreSessions := false;
  nextRandom     := 0;
  nextNonce      := 0;
  nextSession    := 0;

  -- Signature authority's verification key
  undefine authKey;
  authKey.kType  := K_VERIFY;
  authKey.random := freshRandom();

  -- Initialize clients
  undefine cli;
  for i: ClientId do

      cli[i].version    := MaxVersion;
      cli[i].suite.text := 0;
      cli[i].authKey    := authKey;

      -- Initialize verification key
      undefine verifKey;
      verifKey.key.kType  := K_VERIFY;
      verifKey.key.random := freshRandom();
      verifKey.cert.key     := verifKey.key;
      verifKey.cert.owner   := i;
      verifKey.cert.signKey := authKey;
      cli[i].verifKey := verifKey;

      -- Initialize client's secret
      undefine secretKey;
      secretKey.kType  := K_ENCRYPT;
      secretKey.random := freshRandom();
      cli[i].secretKey := secretKey;

      -- Initialize state
      cli[i].state := M_SLEEP;
      cli[i].session := 0;
      cli[i].resumeSession := false;

  end;

  -- Initialize servers
  undefine ser;
  for i: ServerId do

      ser[i].version    := MaxVersion;
      ser[i].suite.text := 0;
      ser[i].authKey    := authKey;

      -- Initialize public key
      undefine publicKey;
      publicKey.key.kType  := K_ENCRYPT;
      publicKey.key.random := freshRandom();
      publicKey.cert.key     := publicKey.key;
      publicKey.cert.owner   := i;
      publicKey.cert.signKey := authKey;
      ser[i].publicKey := publicKey;

      -- Initialize verification key
      undefine verifKey;
      verifKey.key.kType  := K_VERIFY;
      verifKey.key.random := freshRandom();
      verifKey.cert.key     := verifKey.key;
      verifKey.cert.owner   := i;
      verifKey.cert.signKey := authKey;
      ser[i].verifKey := verifKey;

      -- Initialize state
      for j: SessionId do
          for k: MessageType do
              ser[i].clients[j].state := M_SLEEP;
          end;
      end;
      ser[i].clients[0].state := M_CLIENT_HELLO;

  end;

  -- Initialize intruders
  undefine int;
  for i: IntruderId do

	int[i].goodVersion    := MaxVersion;
      int[i].evilVersion    := MaxVersion - 1;
      int[i].goodSuite.text := 0;
      int[i].evilSuite.text := 1;

      -- Initialize nonce
      nonce := freshNonce();

      -- Initialize encryption key
      undefine publicKey;
      publicKey.key.kType  := K_ENCRYPT;
      publicKey.key.random := freshRandom();
      publicKey.cert.key     := publicKey.key;
      publicKey.cert.owner   := i;
      publicKey.cert.signKey := authKey;
      int[i].publicKey := publicKey;

      -- Initialize verification key
      undefine verifKey;
      verifKey.key.kType  := K_VERIFY;
      verifKey.key.random := freshRandom();
      verifKey.cert.key     := verifKey.key;
      verifKey.cert.owner   := i;
      verifKey.cert.signKey := authKey;
      int[i].verifKey := verifKey;

      -- Initialize secret key
      undefine secretKey;
      secretKey.kType  := K_ENCRYPT;
      secretKey.random := freshRandom();

      -- Add its own nonces and keys to the list of known things
      -- (this simplifies rules since multisets are never empty)
      multisetadd(nonce, int[i].nonces);
      multisetadd(int[i].publicKey, int[i].publicKeys);
      multisetadd(int[i].verifKey, int[i].verifKeys);
      multisetadd(secretKey, int[i].secretKeys);
  end;

  -- Initialize network
  undefine cliNet;
  undefine serNet;

end; -- startstate


-- 
-- Correctness conditions
--

-- Intruder knows the client's secret key

ruleset i: ClientId do
  ruleset j: IntruderId do
    rule "Intruder has learned a client's secret"
      cli[i].state = M_DONE &
      multisetcount(s: int[j].secretKeys,
         keyEqual(int[j].secretKeys[s], cli[i].secretKey)) > 0
    ==>
    begin
      error "Intruder has learned a client's secret"
    end;
  end;
end;

-- Intruder knows the server's secret key

ruleset i: ServerId do
  ruleset s: SessionId do
    ruleset j: IntruderId do
      rule "Intruder has learned a server's secret"
        ser[i].clients[s].state = M_DONE &
        !ismember(ser[i].clients[s].client, IntruderId) &
        multisetcount(k: int[j].secretKeys,
           keyEqual(int[j].secretKeys[k], ser[i].clients[s].secretKey)) > 0
      ==>
      begin
        error "Intruder has learned a server's secret"
      end;
    end;
  end;
end;

-- Consistent mutual identification

invariant "If C is talking to S, S is talking to C"
  forall i: ClientId do
    ismember(cli[i].server, ServerId) &
    cli[i].state = M_DONE
    ->
    ser[cli[i].server].clients[cli[i].session].client = i &
    ((cli[i].serverVersion = MaxVersion ->
    ser[cli[i].server].clients[cli[i].session].state =
                              M_CLIENT_FINISHED) |
     (cli[i].serverVersion != MaxVersion ->
    ser[cli[i].server].clients[cli[i].session].state =
                              M_CLIENT_KEY_EXCHANGE) |
    ser[cli[i].server].clients[cli[i].session].state = 
                              M_DONE)
  end;

ruleset i: ServerId do
  ruleset s: SessionId do
    rule "S is talking to C, but C is not talking to S"
      ismember(ser[i].clients[s].client, ClientId) &

      -- Server is done
      ser[i].clients[s].state = M_DONE &

      -- Client doesn't think it's talking to server
      (cli[ser[i].clients[s].client].server != i |

      -- Client (3.0) is not done
      (cli[ser[i].clients[s].client].serverVersion = MaxVersion &
       cli[ser[i].clients[s].client].state != M_DONE) |

      -- Client (2.0) is not waiting for ServerFinished
      (cli[ser[i].clients[s].client].serverVersion != MaxVersion &
       cli[ser[i].clients[s].client].state != M_2_SERVER_FINISHED))
    ==>
    begin
      error "S is talking to C, but C is not talking to S"
    end;
  end;
end;

--
--  Shared secret consistency
--

ruleset i: ClientId do
  rule "Client's shared secret is not known by its server"
    ismember(cli[i].server, ServerId) &
    cli[i].state = M_DONE &
    ser[cli[i].server].clients[cli[i].session].state = M_DONE
  ==>
  begin
    alias k: ser[cli[i].server].clients[cli[i].session].secretKey do
      if isundefined(k.kType) |
         !keyEqual(k, cli[i].secretKey) then
         error "C's secret key is not the same as S's";
      end;
    end;
  end;
end;

ruleset i: ServerId do
  ruleset s: SessionId do
    rule "Server's shared secret is not the same as its client's"
      ismember(ser[i].clients[s].client, ClientId) &
      ser[i].clients[s].state = M_DONE &
      cli[ser[i].clients[s].client].state = M_DONE &
      !keyEqual(cli[ser[i].clients[s].client].secretKey, ser[i].clients[s].secretKey)
    ==>
    begin
      error "S's secret key is not the same as C's"
    end;
  end;
end;

--
-- Attack against versions, suites, etc.
--

invariant "Client has learned the server version and suite correctly"
  forall i: ClientId do
     cli[i].state = M_DONE &
     ser[cli[i].server].clients[cli[i].session].state = M_DONE
     ->
     cli[i].serverVersion = MaxVersion &
     cli[i].serverSuite.text = 0
  end;

ruleset i: ServerId do
  ruleset s: SessionId do
    rule "Server has not learned the client's version or suite correctly"
      !ismember(ser[i].clients[s].client, IntruderId) &
      ser[i].clients[s].state = M_DONE &
      cli[ser[i].clients[s].client].state = M_DONE &
      (ser[i].clients[s].clientVersion != MaxVersion |
       ser[i].clients[s].clientSuite.text != 0)
    ==>
    begin
      error "Server has not learned the client's version or suite correctly"
    end;
  end;
end;

